$\forall$${\it es}$:ES, $e_{1}$, $e_{2}$, $b$:E, $Q$:(\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} $\rightarrow$\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} $\rightarrow\mathbb{P}$).
\\[0ex]($e_{1}$ $<$loc $b$)
\\[0ex]$\Rightarrow$ $b$ $\leq$loc $e_{2}$ 
\\[0ex]$\Rightarrow$ [$e_{1}$,pred($b$)]$\sim$([$a$,$b$].$Q$($a$,$b$))+
\\[0ex]$\Rightarrow$ [$b$,$e_{2}$]$\sim$([$a$,$b$].$Q$($a$,$b$))+
\\[0ex]$\Rightarrow$ [$e_{1}$,$e_{2}$]$\sim$([$a$,$b$].$Q$($a$,$b$))+